; COMMAND-LINE: --incremental
; EXPECT: unsat
; EXPECT: sat
; EXPECT: unsat
; EXPECT: unsat

(set-logic QF_UFLIA)
(declare-fun _base () Int)
(declare-fun _n () Int)
(assert (let ((.def_5 (<= 0 _n)))
.def_5
))
(declare-fun ___z2z___ (Int) Bool)
(declare-fun ___z3z___ (Int) Bool)
(declare-fun ___z4z___ (Int) Bool)
(declare-fun ___z5z___ (Int) Bool)
(declare-fun ___z6z___ (Int) Bool)
(declare-fun ___z7z___ (Int) Int)
(declare-fun ___z8z___ (Int) Int)
(declare-fun ___z9z___ (Int) Int)
(push 1)
(assert (let ((.def_152 (___z4z___ 0)))
(let ((.def_150 (= _base 0)))
(let ((.def_147 (___z6z___ (- 1))))
(let ((.def_148 (not .def_147)))
(let ((.def_145 (___z5z___ 0)))
(let ((.def_146 (not .def_145)))
(let ((.def_149 (and .def_146 .def_148)))
(let ((.def_151 (or .def_149 .def_150)))
(let ((.def_153 (= .def_151 .def_152)))
.def_153
))))))))))
(assert (let ((.def_157 (___z7z___ 0)))
(let ((.def_161 (<= .def_157 (- 10))))
(let ((.def_155 (___z5z___ (- 1))))
(let ((.def_162 (or .def_155 .def_161)))
(let ((.def_158 (<= 0 .def_157)))
(let ((.def_159 (not .def_158)))
(let ((.def_156 (not .def_155)))
(let ((.def_160 (or .def_156 .def_159)))
(let ((.def_163 (and .def_160 .def_162)))
(let ((.def_150 (= _base 0)))
(let ((.def_164 (or .def_150 .def_163)))
(let ((.def_154 (not .def_150)))
(let ((.def_165 (and .def_154 .def_164)))
(let ((.def_145 (___z5z___ 0)))
(let ((.def_166 (= .def_145 .def_165)))
.def_166
))))))))))))))))
(assert (let ((.def_175 (___z6z___ 0)))
(let ((.def_157 (___z7z___ 0)))
(let ((.def_170 (<= 10 .def_157)))
(let ((.def_147 (___z6z___ (- 1))))
(let ((.def_171 (or .def_147 .def_170)))
(let ((.def_167 (<= .def_157 0)))
(let ((.def_168 (not .def_167)))
(let ((.def_148 (not .def_147)))
(let ((.def_169 (or .def_148 .def_168)))
(let ((.def_172 (and .def_169 .def_171)))
(let ((.def_150 (= _base 0)))
(let ((.def_173 (or .def_150 .def_172)))
(let ((.def_154 (not .def_150)))
(let ((.def_174 (and .def_154 .def_173)))
(let ((.def_176 (= .def_174 .def_175)))
.def_176
))))))))))))))))
(assert (let ((.def_177 (___z9z___ 0)))
(let ((.def_178 (___z8z___ 0)))
(let ((.def_179 (+ .def_177 .def_178)))
(let ((.def_181 (___z2z___ 0)))
(let ((.def_180 (___z3z___ 0)))
(let ((.def_182 (and .def_180 .def_181)))
(let ((.def_183 (ite .def_182 .def_179 .def_177)))
(let ((.def_157 (___z7z___ 0)))
(let ((.def_184 (= .def_157 .def_183)))
.def_184
))))))))))
(assert (let ((.def_181 (___z2z___ 0)))
(let ((.def_185 (not .def_181)))
(let ((.def_180 (___z3z___ 0)))
(let ((.def_186 (and .def_180 .def_185)))
(let ((.def_187 (ite .def_186 2 0)))
(let ((.def_188 (not .def_180)))
(let ((.def_189 (and .def_181 .def_188)))
(let ((.def_190 (ite .def_189 1 .def_187)))
(let ((.def_178 (___z8z___ 0)))
(let ((.def_191 (= .def_178 .def_190)))
.def_191
)))))))))))
(assert (let ((.def_192 (___z7z___ (- 1))))
(let ((.def_150 (= _base 0)))
(let ((.def_193 (ite .def_150 0 .def_192)))
(let ((.def_177 (___z9z___ 0)))
(let ((.def_194 (= .def_177 .def_193)))
.def_194
))))))
(assert (let ((.def_201 (___z4z___ (- 1))))
(let ((.def_199 (= _base (- 1))))
(let ((.def_196 (___z6z___ (- 2))))
(let ((.def_197 (not .def_196)))
(let ((.def_155 (___z5z___ (- 1))))
(let ((.def_156 (not .def_155)))
(let ((.def_198 (and .def_156 .def_197)))
(let ((.def_200 (or .def_198 .def_199)))
(let ((.def_202 (= .def_200 .def_201)))
.def_202
))))))))))
(assert (let ((.def_192 (___z7z___ (- 1))))
(let ((.def_209 (<= .def_192 (- 10))))
(let ((.def_204 (___z5z___ (- 2))))
(let ((.def_210 (or .def_204 .def_209)))
(let ((.def_206 (<= 0 .def_192)))
(let ((.def_207 (not .def_206)))
(let ((.def_205 (not .def_204)))
(let ((.def_208 (or .def_205 .def_207)))
(let ((.def_211 (and .def_208 .def_210)))
(let ((.def_199 (= _base (- 1))))
(let ((.def_212 (or .def_199 .def_211)))
(let ((.def_203 (not .def_199)))
(let ((.def_213 (and .def_203 .def_212)))
(let ((.def_155 (___z5z___ (- 1))))
(let ((.def_214 (= .def_155 .def_213)))
.def_214
))))))))))))))))
(assert (let ((.def_192 (___z7z___ (- 1))))
(let ((.def_218 (<= 10 .def_192)))
(let ((.def_196 (___z6z___ (- 2))))
(let ((.def_219 (or .def_196 .def_218)))
(let ((.def_215 (<= .def_192 0)))
(let ((.def_216 (not .def_215)))
(let ((.def_197 (not .def_196)))
(let ((.def_217 (or .def_197 .def_216)))
(let ((.def_220 (and .def_217 .def_219)))
(let ((.def_199 (= _base (- 1))))
(let ((.def_221 (or .def_199 .def_220)))
(let ((.def_203 (not .def_199)))
(let ((.def_222 (and .def_203 .def_221)))
(let ((.def_147 (___z6z___ (- 1))))
(let ((.def_223 (= .def_147 .def_222)))
.def_223
))))))))))))))))
(assert (let ((.def_224 (___z9z___ (- 1))))
(let ((.def_225 (___z8z___ (- 1))))
(let ((.def_226 (+ .def_224 .def_225)))
(let ((.def_228 (___z2z___ (- 1))))
(let ((.def_227 (___z3z___ (- 1))))
(let ((.def_229 (and .def_227 .def_228)))
(let ((.def_230 (ite .def_229 .def_226 .def_224)))
(let ((.def_192 (___z7z___ (- 1))))
(let ((.def_231 (= .def_192 .def_230)))
.def_231
))))))))))
(assert (let ((.def_228 (___z2z___ (- 1))))
(let ((.def_232 (not .def_228)))
(let ((.def_227 (___z3z___ (- 1))))
(let ((.def_233 (and .def_227 .def_232)))
(let ((.def_234 (ite .def_233 2 0)))
(let ((.def_235 (not .def_227)))
(let ((.def_236 (and .def_228 .def_235)))
(let ((.def_237 (ite .def_236 1 .def_234)))
(let ((.def_225 (___z8z___ (- 1))))
(let ((.def_238 (= .def_225 .def_237)))
.def_238
)))))))))))
(assert (let ((.def_239 (___z7z___ (- 2))))
(let ((.def_199 (= _base (- 1))))
(let ((.def_240 (ite .def_199 0 .def_239)))
(let ((.def_224 (___z9z___ (- 1))))
(let ((.def_241 (= .def_224 .def_240)))
.def_241
))))))
(push 1)
(assert (let ((.def_201 (___z4z___ (- 1))))
(let ((.def_152 (___z4z___ 0)))
(let ((.def_242 (and .def_152 .def_201)))
(let ((.def_199 (= _base (- 1))))
(let ((.def_203 (not .def_199)))
(let ((.def_243 (or .def_203 .def_242)))
(let ((.def_244 (not .def_243)))
.def_244
))))))))
(assert true
)
(check-sat)
(pop 1)
(assert (let ((.def_201 (___z4z___ (- 1))))
.def_201
))
(assert (let ((.def_245 (___z4z___ (- 2))))
.def_245
))
(push 1)
(assert (let ((.def_254 (___z4z___ _n)))
(let ((.def_252 (= _n _base)))
(let ((.def_248 (+ _n (- 1))))
(let ((.def_249 (___z6z___ .def_248)))
(let ((.def_250 (not .def_249)))
(let ((.def_246 (___z5z___ _n)))
(let ((.def_247 (not .def_246)))
(let ((.def_251 (and .def_247 .def_250)))
(let ((.def_253 (or .def_251 .def_252)))
(let ((.def_255 (= .def_253 .def_254)))
.def_255
)))))))))))
(assert (let ((.def_259 (___z7z___ _n)))
(let ((.def_263 (<= .def_259 (- 10))))
(let ((.def_248 (+ _n (- 1))))
(let ((.def_257 (___z5z___ .def_248)))
(let ((.def_264 (or .def_257 .def_263)))
(let ((.def_260 (<= 0 .def_259)))
(let ((.def_261 (not .def_260)))
(let ((.def_258 (not .def_257)))
(let ((.def_262 (or .def_258 .def_261)))
(let ((.def_265 (and .def_262 .def_264)))
(let ((.def_252 (= _n _base)))
(let ((.def_266 (or .def_252 .def_265)))
(let ((.def_256 (not .def_252)))
(let ((.def_267 (and .def_256 .def_266)))
(let ((.def_246 (___z5z___ _n)))
(let ((.def_268 (= .def_246 .def_267)))
.def_268
)))))))))))))))))
(assert (let ((.def_277 (___z6z___ _n)))
(let ((.def_259 (___z7z___ _n)))
(let ((.def_272 (<= 10 .def_259)))
(let ((.def_248 (+ _n (- 1))))
(let ((.def_249 (___z6z___ .def_248)))
(let ((.def_273 (or .def_249 .def_272)))
(let ((.def_269 (<= .def_259 0)))
(let ((.def_270 (not .def_269)))
(let ((.def_250 (not .def_249)))
(let ((.def_271 (or .def_250 .def_270)))
(let ((.def_274 (and .def_271 .def_273)))
(let ((.def_252 (= _n _base)))
(let ((.def_275 (or .def_252 .def_274)))
(let ((.def_256 (not .def_252)))
(let ((.def_276 (and .def_256 .def_275)))
(let ((.def_278 (= .def_276 .def_277)))
.def_278
)))))))))))))))))
(assert (let ((.def_279 (___z9z___ _n)))
(let ((.def_280 (___z8z___ _n)))
(let ((.def_281 (+ .def_279 .def_280)))
(let ((.def_283 (___z2z___ _n)))
(let ((.def_282 (___z3z___ _n)))
(let ((.def_284 (and .def_282 .def_283)))
(let ((.def_285 (ite .def_284 .def_281 .def_279)))
(let ((.def_259 (___z7z___ _n)))
(let ((.def_286 (= .def_259 .def_285)))
.def_286
))))))))))
(assert (let ((.def_283 (___z2z___ _n)))
(let ((.def_287 (not .def_283)))
(let ((.def_282 (___z3z___ _n)))
(let ((.def_288 (and .def_282 .def_287)))
(let ((.def_289 (ite .def_288 2 0)))
(let ((.def_290 (not .def_282)))
(let ((.def_291 (and .def_283 .def_290)))
(let ((.def_292 (ite .def_291 1 .def_289)))
(let ((.def_280 (___z8z___ _n)))
(let ((.def_293 (= .def_280 .def_292)))
.def_293
)))))))))))
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_294 (___z7z___ .def_248)))
(let ((.def_252 (= _n _base)))
(let ((.def_295 (ite .def_252 0 .def_294)))
(let ((.def_279 (___z9z___ _n)))
(let ((.def_296 (= .def_279 .def_295)))
.def_296
)))))))
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_305 (___z4z___ .def_248)))
(let ((.def_301 (* (- 1) _base)))
(let ((.def_302 (+ _n .def_301)))
(let ((.def_303 (= .def_302 1)))
(let ((.def_297 (+ (- 1) .def_248)))
(let ((.def_298 (___z6z___ .def_297)))
(let ((.def_299 (not .def_298)))
(let ((.def_257 (___z5z___ .def_248)))
(let ((.def_258 (not .def_257)))
(let ((.def_300 (and .def_258 .def_299)))
(let ((.def_304 (or .def_300 .def_303)))
(let ((.def_306 (= .def_304 .def_305)))
.def_306
))))))))))))))
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_294 (___z7z___ .def_248)))
(let ((.def_313 (<= .def_294 (- 10))))
(let ((.def_297 (+ (- 1) .def_248)))
(let ((.def_308 (___z5z___ .def_297)))
(let ((.def_314 (or .def_308 .def_313)))
(let ((.def_310 (<= 0 .def_294)))
(let ((.def_311 (not .def_310)))
(let ((.def_309 (not .def_308)))
(let ((.def_312 (or .def_309 .def_311)))
(let ((.def_315 (and .def_312 .def_314)))
(let ((.def_301 (* (- 1) _base)))
(let ((.def_302 (+ _n .def_301)))
(let ((.def_303 (= .def_302 1)))
(let ((.def_316 (or .def_303 .def_315)))
(let ((.def_307 (not .def_303)))
(let ((.def_317 (and .def_307 .def_316)))
(let ((.def_257 (___z5z___ .def_248)))
(let ((.def_318 (= .def_257 .def_317)))
.def_318
))))))))))))))))))))
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_294 (___z7z___ .def_248)))
(let ((.def_322 (<= 10 .def_294)))
(let ((.def_297 (+ (- 1) .def_248)))
(let ((.def_298 (___z6z___ .def_297)))
(let ((.def_323 (or .def_298 .def_322)))
(let ((.def_319 (<= .def_294 0)))
(let ((.def_320 (not .def_319)))
(let ((.def_299 (not .def_298)))
(let ((.def_321 (or .def_299 .def_320)))
(let ((.def_324 (and .def_321 .def_323)))
(let ((.def_301 (* (- 1) _base)))
(let ((.def_302 (+ _n .def_301)))
(let ((.def_303 (= .def_302 1)))
(let ((.def_325 (or .def_303 .def_324)))
(let ((.def_307 (not .def_303)))
(let ((.def_326 (and .def_307 .def_325)))
(let ((.def_249 (___z6z___ .def_248)))
(let ((.def_327 (= .def_249 .def_326)))
.def_327
))))))))))))))))))))
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_328 (___z9z___ .def_248)))
(let ((.def_329 (___z8z___ .def_248)))
(let ((.def_330 (+ .def_328 .def_329)))
(let ((.def_332 (___z2z___ .def_248)))
(let ((.def_331 (___z3z___ .def_248)))
(let ((.def_333 (and .def_331 .def_332)))
(let ((.def_334 (ite .def_333 .def_330 .def_328)))
(let ((.def_294 (___z7z___ .def_248)))
(let ((.def_335 (= .def_294 .def_334)))
.def_335
)))))))))))
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_332 (___z2z___ .def_248)))
(let ((.def_336 (not .def_332)))
(let ((.def_331 (___z3z___ .def_248)))
(let ((.def_337 (and .def_331 .def_336)))
(let ((.def_338 (ite .def_337 2 0)))
(let ((.def_339 (not .def_331)))
(let ((.def_340 (and .def_332 .def_339)))
(let ((.def_341 (ite .def_340 1 .def_338)))
(let ((.def_329 (___z8z___ .def_248)))
(let ((.def_342 (= .def_329 .def_341)))
.def_342
))))))))))))
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_297 (+ (- 1) .def_248)))
(let ((.def_343 (___z7z___ .def_297)))
(let ((.def_301 (* (- 1) _base)))
(let ((.def_302 (+ _n .def_301)))
(let ((.def_303 (= .def_302 1)))
(let ((.def_344 (ite .def_303 0 .def_343)))
(let ((.def_328 (___z9z___ .def_248)))
(let ((.def_345 (= .def_328 .def_344)))
.def_345
))))))))))
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_305 (___z4z___ .def_248)))
.def_305
)))
(assert (let ((.def_254 (___z4z___ _n)))
(let ((.def_199 (= _base (- 1))))
(let ((.def_203 (not .def_199)))
(let ((.def_346 (or .def_203 .def_254)))
(let ((.def_347 (not .def_346)))
.def_347
))))))
(assert true
)
(check-sat)
(pop 1)
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_305 (___z4z___ .def_248)))
.def_305
)))
(assert (let ((.def_348 (+ _n (- 2))))
(let ((.def_349 (___z4z___ .def_348)))
.def_349
)))
(assert (let ((.def_354 (= _base (- 2))))
(let ((.def_351 (___z6z___ (- 3))))
(let ((.def_352 (not .def_351)))
(let ((.def_204 (___z5z___ (- 2))))
(let ((.def_205 (not .def_204)))
(let ((.def_353 (and .def_205 .def_352)))
(let ((.def_355 (or .def_353 .def_354)))
(let ((.def_245 (___z4z___ (- 2))))
(let ((.def_356 (= .def_245 .def_355)))
.def_356
))))))))))
(assert (let ((.def_239 (___z7z___ (- 2))))
(let ((.def_363 (<= .def_239 (- 10))))
(let ((.def_358 (___z5z___ (- 3))))
(let ((.def_364 (or .def_358 .def_363)))
(let ((.def_360 (<= 0 .def_239)))
(let ((.def_361 (not .def_360)))
(let ((.def_359 (not .def_358)))
(let ((.def_362 (or .def_359 .def_361)))
(let ((.def_365 (and .def_362 .def_364)))
(let ((.def_354 (= _base (- 2))))
(let ((.def_366 (or .def_354 .def_365)))
(let ((.def_357 (not .def_354)))
(let ((.def_367 (and .def_357 .def_366)))
(let ((.def_204 (___z5z___ (- 2))))
(let ((.def_368 (= .def_204 .def_367)))
.def_368
))))))))))))))))
(assert (let ((.def_239 (___z7z___ (- 2))))
(let ((.def_372 (<= 10 .def_239)))
(let ((.def_351 (___z6z___ (- 3))))
(let ((.def_373 (or .def_351 .def_372)))
(let ((.def_369 (<= .def_239 0)))
(let ((.def_370 (not .def_369)))
(let ((.def_352 (not .def_351)))
(let ((.def_371 (or .def_352 .def_370)))
(let ((.def_374 (and .def_371 .def_373)))
(let ((.def_354 (= _base (- 2))))
(let ((.def_375 (or .def_354 .def_374)))
(let ((.def_357 (not .def_354)))
(let ((.def_376 (and .def_357 .def_375)))
(let ((.def_196 (___z6z___ (- 2))))
(let ((.def_377 (= .def_196 .def_376)))
.def_377
))))))))))))))))
(assert (let ((.def_378 (___z9z___ (- 2))))
(let ((.def_379 (___z8z___ (- 2))))
(let ((.def_380 (+ .def_378 .def_379)))
(let ((.def_382 (___z2z___ (- 2))))
(let ((.def_381 (___z3z___ (- 2))))
(let ((.def_383 (and .def_381 .def_382)))
(let ((.def_384 (ite .def_383 .def_380 .def_378)))
(let ((.def_239 (___z7z___ (- 2))))
(let ((.def_385 (= .def_239 .def_384)))
.def_385
))))))))))
(assert (let ((.def_382 (___z2z___ (- 2))))
(let ((.def_386 (not .def_382)))
(let ((.def_381 (___z3z___ (- 2))))
(let ((.def_387 (and .def_381 .def_386)))
(let ((.def_388 (ite .def_387 2 0)))
(let ((.def_389 (not .def_381)))
(let ((.def_390 (and .def_382 .def_389)))
(let ((.def_391 (ite .def_390 1 .def_388)))
(let ((.def_379 (___z8z___ (- 2))))
(let ((.def_392 (= .def_379 .def_391)))
.def_392
)))))))))))
(assert (let ((.def_393 (___z7z___ (- 3))))
(let ((.def_354 (= _base (- 2))))
(let ((.def_394 (ite .def_354 0 .def_393)))
(let ((.def_378 (___z9z___ (- 2))))
(let ((.def_395 (= .def_378 .def_394)))
.def_395
))))))
(assert (let ((.def_254 (___z4z___ _n)))
(let ((.def_252 (= _n _base)))
(let ((.def_248 (+ _n (- 1))))
(let ((.def_249 (___z6z___ .def_248)))
(let ((.def_250 (not .def_249)))
(let ((.def_246 (___z5z___ _n)))
(let ((.def_247 (not .def_246)))
(let ((.def_251 (and .def_247 .def_250)))
(let ((.def_253 (or .def_251 .def_252)))
(let ((.def_255 (= .def_253 .def_254)))
.def_255
)))))))))))
(assert (let ((.def_259 (___z7z___ _n)))
(let ((.def_263 (<= .def_259 (- 10))))
(let ((.def_248 (+ _n (- 1))))
(let ((.def_257 (___z5z___ .def_248)))
(let ((.def_264 (or .def_257 .def_263)))
(let ((.def_260 (<= 0 .def_259)))
(let ((.def_261 (not .def_260)))
(let ((.def_258 (not .def_257)))
(let ((.def_262 (or .def_258 .def_261)))
(let ((.def_265 (and .def_262 .def_264)))
(let ((.def_252 (= _n _base)))
(let ((.def_266 (or .def_252 .def_265)))
(let ((.def_256 (not .def_252)))
(let ((.def_267 (and .def_256 .def_266)))
(let ((.def_246 (___z5z___ _n)))
(let ((.def_268 (= .def_246 .def_267)))
.def_268
)))))))))))))))))
(assert (let ((.def_277 (___z6z___ _n)))
(let ((.def_259 (___z7z___ _n)))
(let ((.def_272 (<= 10 .def_259)))
(let ((.def_248 (+ _n (- 1))))
(let ((.def_249 (___z6z___ .def_248)))
(let ((.def_273 (or .def_249 .def_272)))
(let ((.def_269 (<= .def_259 0)))
(let ((.def_270 (not .def_269)))
(let ((.def_250 (not .def_249)))
(let ((.def_271 (or .def_250 .def_270)))
(let ((.def_274 (and .def_271 .def_273)))
(let ((.def_252 (= _n _base)))
(let ((.def_275 (or .def_252 .def_274)))
(let ((.def_256 (not .def_252)))
(let ((.def_276 (and .def_256 .def_275)))
(let ((.def_278 (= .def_276 .def_277)))
.def_278
)))))))))))))))))
(assert (let ((.def_279 (___z9z___ _n)))
(let ((.def_280 (___z8z___ _n)))
(let ((.def_281 (+ .def_279 .def_280)))
(let ((.def_283 (___z2z___ _n)))
(let ((.def_282 (___z3z___ _n)))
(let ((.def_284 (and .def_282 .def_283)))
(let ((.def_285 (ite .def_284 .def_281 .def_279)))
(let ((.def_259 (___z7z___ _n)))
(let ((.def_286 (= .def_259 .def_285)))
.def_286
))))))))))
(assert (let ((.def_283 (___z2z___ _n)))
(let ((.def_287 (not .def_283)))
(let ((.def_282 (___z3z___ _n)))
(let ((.def_288 (and .def_282 .def_287)))
(let ((.def_289 (ite .def_288 2 0)))
(let ((.def_290 (not .def_282)))
(let ((.def_291 (and .def_283 .def_290)))
(let ((.def_292 (ite .def_291 1 .def_289)))
(let ((.def_280 (___z8z___ _n)))
(let ((.def_293 (= .def_280 .def_292)))
.def_293
)))))))))))
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_294 (___z7z___ .def_248)))
(let ((.def_252 (= _n _base)))
(let ((.def_295 (ite .def_252 0 .def_294)))
(let ((.def_279 (___z9z___ _n)))
(let ((.def_296 (= .def_279 .def_295)))
.def_296
)))))))
(push 1)
(assert (let ((.def_354 (= _base (- 2))))
(let ((.def_357 (not .def_354)))
(let ((.def_152 (___z4z___ 0)))
(let ((.def_396 (or .def_152 .def_357)))
(let ((.def_397 (not .def_396)))
.def_397
))))))
(assert true
)
(check-sat)
(pop 1)
(assert (let ((.def_399 (___z4z___ (- 3))))
.def_399
))
(push 1)
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_305 (___z4z___ .def_248)))
(let ((.def_301 (* (- 1) _base)))
(let ((.def_302 (+ _n .def_301)))
(let ((.def_303 (= .def_302 1)))
(let ((.def_297 (+ (- 1) .def_248)))
(let ((.def_298 (___z6z___ .def_297)))
(let ((.def_299 (not .def_298)))
(let ((.def_257 (___z5z___ .def_248)))
(let ((.def_258 (not .def_257)))
(let ((.def_300 (and .def_258 .def_299)))
(let ((.def_304 (or .def_300 .def_303)))
(let ((.def_306 (= .def_304 .def_305)))
.def_306
))))))))))))))
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_294 (___z7z___ .def_248)))
(let ((.def_313 (<= .def_294 (- 10))))
(let ((.def_297 (+ (- 1) .def_248)))
(let ((.def_308 (___z5z___ .def_297)))
(let ((.def_314 (or .def_308 .def_313)))
(let ((.def_310 (<= 0 .def_294)))
(let ((.def_311 (not .def_310)))
(let ((.def_309 (not .def_308)))
(let ((.def_312 (or .def_309 .def_311)))
(let ((.def_315 (and .def_312 .def_314)))
(let ((.def_301 (* (- 1) _base)))
(let ((.def_302 (+ _n .def_301)))
(let ((.def_303 (= .def_302 1)))
(let ((.def_316 (or .def_303 .def_315)))
(let ((.def_307 (not .def_303)))
(let ((.def_317 (and .def_307 .def_316)))
(let ((.def_257 (___z5z___ .def_248)))
(let ((.def_318 (= .def_257 .def_317)))
.def_318
))))))))))))))))))))
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_294 (___z7z___ .def_248)))
(let ((.def_322 (<= 10 .def_294)))
(let ((.def_297 (+ (- 1) .def_248)))
(let ((.def_298 (___z6z___ .def_297)))
(let ((.def_323 (or .def_298 .def_322)))
(let ((.def_319 (<= .def_294 0)))
(let ((.def_320 (not .def_319)))
(let ((.def_299 (not .def_298)))
(let ((.def_321 (or .def_299 .def_320)))
(let ((.def_324 (and .def_321 .def_323)))
(let ((.def_301 (* (- 1) _base)))
(let ((.def_302 (+ _n .def_301)))
(let ((.def_303 (= .def_302 1)))
(let ((.def_325 (or .def_303 .def_324)))
(let ((.def_307 (not .def_303)))
(let ((.def_326 (and .def_307 .def_325)))
(let ((.def_249 (___z6z___ .def_248)))
(let ((.def_327 (= .def_249 .def_326)))
.def_327
))))))))))))))))))))
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_328 (___z9z___ .def_248)))
(let ((.def_329 (___z8z___ .def_248)))
(let ((.def_330 (+ .def_328 .def_329)))
(let ((.def_332 (___z2z___ .def_248)))
(let ((.def_331 (___z3z___ .def_248)))
(let ((.def_333 (and .def_331 .def_332)))
(let ((.def_334 (ite .def_333 .def_330 .def_328)))
(let ((.def_294 (___z7z___ .def_248)))
(let ((.def_335 (= .def_294 .def_334)))
.def_335
)))))))))))
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_332 (___z2z___ .def_248)))
(let ((.def_336 (not .def_332)))
(let ((.def_331 (___z3z___ .def_248)))
(let ((.def_337 (and .def_331 .def_336)))
(let ((.def_338 (ite .def_337 2 0)))
(let ((.def_339 (not .def_331)))
(let ((.def_340 (and .def_332 .def_339)))
(let ((.def_341 (ite .def_340 1 .def_338)))
(let ((.def_329 (___z8z___ .def_248)))
(let ((.def_342 (= .def_329 .def_341)))
.def_342
))))))))))))
(assert (let ((.def_248 (+ _n (- 1))))
(let ((.def_297 (+ (- 1) .def_248)))
(let ((.def_343 (___z7z___ .def_297)))
(let ((.def_301 (* (- 1) _base)))
(let ((.def_302 (+ _n .def_301)))
(let ((.def_303 (= .def_302 1)))
(let ((.def_344 (ite .def_303 0 .def_343)))
(let ((.def_328 (___z9z___ .def_248)))
(let ((.def_345 (= .def_328 .def_344)))
.def_345
))))))))))
(assert (let ((.def_301 (* (- 1) _base)))
(let ((.def_302 (+ _n .def_301)))
(let ((.def_406 (= .def_302 2)))
(let ((.def_348 (+ _n (- 2))))
(let ((.def_402 (+ (- 1) .def_348)))
(let ((.def_403 (___z6z___ .def_402)))
(let ((.def_404 (not .def_403)))
(let ((.def_400 (___z5z___ .def_348)))
(let ((.def_401 (not .def_400)))
(let ((.def_405 (and .def_401 .def_404)))
(let ((.def_407 (or .def_405 .def_406)))
(let ((.def_349 (___z4z___ .def_348)))
(let ((.def_408 (= .def_349 .def_407)))
.def_408
))))))))))))))
(assert (let ((.def_348 (+ _n (- 2))))
(let ((.def_412 (___z7z___ .def_348)))
(let ((.def_416 (<= .def_412 (- 10))))
(let ((.def_402 (+ (- 1) .def_348)))
(let ((.def_410 (___z5z___ .def_402)))
(let ((.def_417 (or .def_410 .def_416)))
(let ((.def_413 (<= 0 .def_412)))
(let ((.def_414 (not .def_413)))
(let ((.def_411 (not .def_410)))
(let ((.def_415 (or .def_411 .def_414)))
(let ((.def_418 (and .def_415 .def_417)))
(let ((.def_301 (* (- 1) _base)))
(let ((.def_302 (+ _n .def_301)))
(let ((.def_406 (= .def_302 2)))
(let ((.def_419 (or .def_406 .def_418)))
(let ((.def_409 (not .def_406)))
(let ((.def_420 (and .def_409 .def_419)))
(let ((.def_400 (___z5z___ .def_348)))
(let ((.def_421 (= .def_400 .def_420)))
.def_421
))))))))))))))))))))
(assert (let ((.def_348 (+ _n (- 2))))
(let ((.def_430 (___z6z___ .def_348)))
(let ((.def_412 (___z7z___ .def_348)))
(let ((.def_425 (<= 10 .def_412)))
(let ((.def_402 (+ (- 1) .def_348)))
(let ((.def_403 (___z6z___ .def_402)))
(let ((.def_426 (or .def_403 .def_425)))
(let ((.def_422 (<= .def_412 0)))
(let ((.def_423 (not .def_422)))
(let ((.def_404 (not .def_403)))
(let ((.def_424 (or .def_404 .def_423)))
(let ((.def_427 (and .def_424 .def_426)))
(let ((.def_301 (* (- 1) _base)))
(let ((.def_302 (+ _n .def_301)))
(let ((.def_406 (= .def_302 2)))
(let ((.def_428 (or .def_406 .def_427)))
(let ((.def_409 (not .def_406)))
(let ((.def_429 (and .def_409 .def_428)))
(let ((.def_431 (= .def_429 .def_430)))
.def_431
))))))))))))))))))))
(assert (let ((.def_348 (+ _n (- 2))))
(let ((.def_432 (___z9z___ .def_348)))
(let ((.def_433 (___z8z___ .def_348)))
(let ((.def_434 (+ .def_432 .def_433)))
(let ((.def_436 (___z2z___ .def_348)))
(let ((.def_435 (___z3z___ .def_348)))
(let ((.def_437 (and .def_435 .def_436)))
(let ((.def_438 (ite .def_437 .def_434 .def_432)))
(let ((.def_412 (___z7z___ .def_348)))
(let ((.def_439 (= .def_412 .def_438)))
.def_439
)))))))))))
(assert (let ((.def_348 (+ _n (- 2))))
(let ((.def_436 (___z2z___ .def_348)))
(let ((.def_440 (not .def_436)))
(let ((.def_435 (___z3z___ .def_348)))
(let ((.def_441 (and .def_435 .def_440)))
(let ((.def_442 (ite .def_441 2 0)))
(let ((.def_443 (not .def_435)))
(let ((.def_444 (and .def_436 .def_443)))
(let ((.def_445 (ite .def_444 1 .def_442)))
(let ((.def_433 (___z8z___ .def_348)))
(let ((.def_446 (= .def_433 .def_445)))
.def_446
))))))))))))
(assert (let ((.def_348 (+ _n (- 2))))
(let ((.def_402 (+ (- 1) .def_348)))
(let ((.def_447 (___z7z___ .def_402)))
(let ((.def_301 (* (- 1) _base)))
(let ((.def_302 (+ _n .def_301)))
(let ((.def_406 (= .def_302 2)))
(let ((.def_448 (ite .def_406 0 .def_447)))
(let ((.def_432 (___z9z___ .def_348)))
(let ((.def_449 (= .def_432 .def_448)))
.def_449
))))))))))
(assert (let ((.def_354 (= _base (- 2))))
(let ((.def_357 (not .def_354)))
(let ((.def_254 (___z4z___ _n)))
(let ((.def_450 (or .def_254 .def_357)))
(let ((.def_451 (not .def_450)))
.def_451
))))))
(assert true
)
(check-sat)
